es:ES, A:Type, i:Id, ds:x:Id fp Type, conds:k:Knd fp V:Type  (State(ds)V(A + Top)).
(k:Knd. (k  dom(conds))  (hasloc(k;i)))
 (e:E.
 (loc(e) = i)
  (kind(e)  dom(conds))
  ((valtype(e) r (conds(kind(e)).1))
  & ((k:Knd. (k  dom(conds)))  (state@loc(e) r State(ds)))))
 (es-triggers(es;i;ds;conds)  AbsInterface(A)) 

latex

Definitions

x:A. B(x), P  Q, P & Q, x:A. B(x), t  T, AbsInterface(A), es-triggers(es;i;ds;conds), x. t(x), if b then t else f fi , p  q, tt, ff, , x(s), , Unit, P  Q, P  Q,

Lemmas

es-E wf, Id wf, es-loc wf, assert wf, fpf-dom wf, Knd wf, Kind-deq wf, fpf-trivial-subtype-top, decl-state wf, top wf, es-kind wf, es-valtype wf, pi1 wf, fpf-ap wf, es-state wf, hasloc wf, fpf wf, event system wf, bool wf, eqtt to assert, iff transitivity, assert-eq-id, pi2 wf, es-state-when wf, es-state-subtype, es-state-subtype-iff, es-val wf, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff